1 /-
2 Copyright (c) 2019 Kenny Lau, Chris Hughes. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Kenny Lau, Chris Hughes
5
6 Direct limit of modules, abelian groups, rings, and fields.
7
8 See Atiyah-Macdonald PP.32-33, Matsumura PP.269-270
9
10 Generalizes the notion of "union", or "gluing", of incomparable modules over the same ring,
11 or incomparable abelian groups, or rings, or fields.
12
13 It is constructed as a quotient of the free module (for the module case) or quotient of
14 the free commutative ring (for the ring case) instead of a quotient of the disjoint union
15 so as to make the operations (addition etc.) "computable".
16 -/
17
18 import linear_algebra.direct_sum_module
src └──────────────────────────────┘
19 import algebra.big_operators
src └───────────────────┘
20 import ring_theory.free_comm_ring
src └────────────────────────┘
21 import ring_theory.ideal_operations
src └──────────────────────────┘
22
23 universes u v w u₁
24
25 open lattice submodule
26
27 variables {R : Type u} [ring R]
id └──┘ └──┘
src └──┘
typ └──┘ └──┘
28 variables {ι : Type v} [nonempty ι]
id └──┘ └──────┘
src └──────┘
typ └──┘ └──────┘
29 variables [directed_order ι] [decidable_eq ι]
id └────────────┘ └──────────┘
src └────────────┘ └──────────┘
typ └────────────┘ └──────────┘
30 variables (G : ι → Type w) [Π i, decidable_eq (G i)]
id ┴ ┴ └──────────┘ ┴
src └──────────┘
typ ┴ ┴ └──────────┘ ┴
31
32 /-- A directed system is a functor from the category (directed poset) to another category.
33 This is used for abelian groups and rings and fields because their maps are not bundled.
34 See module.directed_system -/
35 class directed_system (f : Π i j, i ≤ j → G i → G j) : Prop :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
36 (map_self : ∀ i x h, f i i h x = x)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
37 (map_map : ∀ i j k hij hjk x, f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x)
id ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └─┘ └─┘ ┴
src ┴ ┴ └──────┘
typ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └─┘ └─┘ ┴
38
39 namespace module
40
41 variables [Π i, add_comm_group (G i)] [Π i, module R (G i)]
id ┴ └────────────┘ ┴ ┴ └────┘ ┴
src └────────────┘ └────┘
typ ┴ └────────────┘ ┴ ┴ └────┘ ┴
doc └────┘
42
43 /-- A directed system is a functor from the category (directed poset) to the category of R-modules. -/
44 class directed_system (f : Π i j, i ≤ j → G i →ₗ[R] G j) : Prop :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴
45 (map_self : ∀ i x h, f i i h x = x)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
46 (map_map : ∀ i j k hij hjk x, f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x)
id ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └─┘ └─┘ ┴
src ┴ ┴ └──────┘
typ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └─┘ └─┘ ┴
47
48 variables (f : Π i j, i ≤ j → G i →ₗ[R] G j) [directed_system G f]
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────────────┘
src ┴ └─┘ ┴ └─────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────────────┘
doc └─────────────┘
49
50 /-- The direct limit of a directed system is the modules glued together along the maps. -/
51 def direct_limit : Type (max v w) :=
52 (span R $ { a | ∃ (i j) (H : i ≤ j) x,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └──┘
53 direct_sum.lof R ι G i x - direct_sum.lof R ι G j (f i j H x) = a }).quotient
id └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src └────────────┘ ┴ └────────────┘ ┴ └──────┘
typ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
doc └──────┘
54
55 namespace direct_limit
56
57 instance : add_comm_group (direct_limit G f) := quotient.add_comm_group _
id └────────────┘ └──────────┘ ┴ ┴ └─────────────────────┘
src └────────────┘ └──────────┘ └─────────────────────┘
typ └────────────┘ └──────────┘ ┴ ┴ └─────────────────────┘
doc └──────────┘
58 instance : module R (direct_limit G f) := quotient.module _
id └────┘ ┴ └──────────┘ ┴ ┴ └─────────────┘
src └────┘ └──────────┘ └─────────────┘
typ └────┘ ┴ └──────────┘ ┴ ┴ └─────────────┘
doc └────┘ └──────────┘
59
60 variables (R ι)
61 /-- The canonical map from a component to the direct limit. -/
62 def of (i) : G i →ₗ[R] direct_limit G f :=
id ┴ ┴ └─┘┴┴ └──────────┘ ┴ ┴
src └─┘ ┴ └──────────┘
typ ┴ ┴ └─┘┴┴ └──────────┘ ┴ ┴
doc └──────────┘
63 (mkq _).comp $ direct_sum.lof R ι G i
id └─┘ └──┘ └────────────┘ ┴ ┴ ┴ ┴
src └─┘ └──┘ └────────────┘
typ └─┘ └──┘ └────────────┘ ┴ ┴ ┴ ┴
doc └─┘
64 variables {R ι G f}
65
66 @[simp] lemma of_f {i j hij x} : (of R ι G f j (f i j hij x)) = of R ι G f i x :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └┘ └┘
67 eq.symm $ (submodule.quotient.eq _).2 $ subset_span ⟨i, j, hij, x, rfl⟩
id └─────┘ └───────────────────┘ ┴ └─────────┘ ┴ ┴ └─┘ ┴ └─┘
src └─────┘ └───────────────────┘ ┴ └─────────┘ └─┘
typ └─────┘ └───────────────────┘ ┴ └─────────┘ ┴ ┴ └─┘ ┴ └─┘
68
69 /-- Every element of the direct limit corresponds to some element in
70 some component of the directed system. -/
71 theorem exists_of (z : direct_limit G f) : ∃ i x, of R ι G f i x = z :=
id └──────────┘ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ └┘ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────┘ └┘
72 nonempty.elim (by apply_instance) $ assume ind : ι,
id └───────────┘ ┴
src └───────────┘ └────────────┘
typ └───────────┘ └────────────┘ ┴
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
73 quotient.induction_on' z $ λ z, direct_sum.induction_on z
id └────────────────────┘ ┴ ┴ └─────────────────────┘ ┴
src └────────────────────┘ └─────────────────────┘
typ └────────────────────┘ ┴ ┴ └─────────────────────┘ ┴
74 ⟨ind, 0, linear_map.map_zero _⟩
id └─┘ └─────────────────┘
src └─────────────────┘
typ └─┘ └─────────────────┘
75 (λ i x, ⟨i, x, rfl⟩)
id ┴ ┴ ┴ ┴ └─┘
src └─┘
typ ┴ ┴ ┴ ┴ └─┘
76 (λ p q ⟨i, x, ihx⟩ ⟨j, y, ihy⟩, let ⟨k, hik, hjk⟩ := directed_order.directed i j in
id ┴ ┴ ┴┴ ┴ ┴┴ ┴ └─┘ ┴ └─┘ └─┘ └─────────────────────┘
src └─────────────────────┘
typ ┴ ┴ ┴┴ ┴ ┴┴ ┴ └─┘ ┴ └─┘ └─┘ └─────────────────────┘
77 ⟨k, f i k hik x + f j k hjk y, by rw [linear_map.map_add, of_f, of_f, ihx, ihy]; refl⟩)
id ┴ ┴ ┴ └────────────────┘ └──┘ └──┘ └─┘ └─┘
src ┴ └──┘└────────────────┘└┘└──┘└┘└──┘└┘ └┘ ┴ └──┘
typ ┴ ┴ ┴ └──┘└────────────────┘└┘└──┘└┘└──┘└┘└─┘└┘└─┘┴ └──┘
doc └──┘ └┘ └┘ └┘ └┘ ┴ └──┘
txt └──┘ └┘ └┘ └┘ └┘ ┴ └──┘
par └──┘ └┘ └┘ └┘ └┘ ┴ └──┘
pid └┘ └┘ └┘ └┘ └┘ ┴
st └─────────────────────┘└────┘└─────────┘└───┘┴└────┘
78
79 @[elab_as_eliminator]
doc └────────────────┘
80 protected theorem induction_on {C : direct_limit G f → Prop} (z : direct_limit G f)
id └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
81 (ih : ∀ i x, C (of R ι G f i x)) : C z :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
82 let ⟨i, x, h⟩ := exists_of z in h ▸ ih i x
id └─┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘
src └───────┘ ┴
typ └─┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘
doc └───────┘
83
84 variables {P : Type u₁} [add_comm_group P] [module R P] (g : Π i, G i →ₗ[R] P)
id └────────────┘ └────┘ ┴ ┴ └─┘ ┴
src └────────────┘ └────┘ └─┘ ┴
typ └────────────┘ └────┘ ┴ ┴ └─┘ ┴
doc └────┘
85 variables (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
86 include Hg
87
88 variables (R ι G f)
89 /-- The universal property of the direct limit: maps from the components to another module
90 that respect the directed system structure (i.e. make some diagram commute) give rise
91 to a unique map out of the direct limit. -/
92 def lift : direct_limit G f →ₗ[R] P :=
id └──────────┘ ┴ ┴ └─┘┴┴ ┴
src └──────────┘ └─┘ ┴
typ └──────────┘ ┴ ┴ └─┘┴┴ ┴
doc └──────────┘
93 liftq _ (direct_sum.to_module R ι P g)
id └───┘ └──────────────────┘ ┴ ┴ ┴ ┴
src └───┘ └──────────────────┘
typ └───┘ └──────────────────┘ ┴ ┴ ┴ ┴
doc └───┘
94 (span_le.2 $ λ a ⟨i, j, hij, x, hx⟩, by rw [← hx, mem_coe, linear_map.sub_mem_ker_iff,
id └─────┘┴ ┴ ┴ └┘ └─────┘ └────────────────────────┘
src └─────┘┴ └────┘ └┘└─────┘└┘└────────────────────────┘└─
typ └─────┘┴ ┴ ┴ └────┘└┘└┘└─────┘└┘└────────────────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid └──┘ └┘ └┘ └─
st └───────┘└───────┘└──────────────────────────┘└─
95 direct_sum.to_module_lof, direct_sum.to_module_lof, Hg])
id └──────────────────────┘ └──────────────────────┘ └┘
src ───┘└──────────────────────┘└┘└──────────────────────┘└┘ ┴
typ ───┘└──────────────────────┘└┘└──────────────────────┘└┘└┘┴
doc ───┘ └┘ └┘ ┴
txt ───┘ └┘ └┘ ┴
par ───┘ └┘ └┘ ┴
pid ───┘ └┘ └┘ ┴
st ───────────────────────────┘└────────────────────────┘└──┘┴
96 variables {R ι G f}
97
98 omit Hg
99 lemma lift_of {i} (x) : lift R ι G f g Hg (of R ι G f i x) = g i x :=
id └──┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └┘
100 direct_sum.to_module_lof R _ _
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
101
102 theorem lift_unique (F : direct_limit G f →ₗ[R] P) (x) :
id └──────────┘ ┴ ┴ └─┘┴┴ ┴
src └──────────┘ └─┘ ┴
typ └──────────┘ ┴ ┴ └─┘┴┴ ┴
doc └──────────┘
103 F x = lift R ι G f (λ i, F.comp $ of R ι G f i)
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ └───┘ └┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └┘
104 (λ i j hij x, by rw [linear_map.comp_apply, of_f]; refl) x :=
id ┴ ┴ └─┘ ┴ └───────────────────┘ ┴ ┴ ┴
src └──┘└───────────────────┘└┘┴ ┴ ┴ └──┘
typ ┴ ┴ └─┘ ┴ └──┘└───────────────────┘└┘┴ ┴ ┴ └──┘ ┴
doc └──┘ └┘ ┴ └──┘
txt └──┘ └┘ ┴ └──┘
par └──┘ └┘ ┴ └──┘
pid └┘ └┘ ┴
st └────────────────────────┘└─┘ ┴ ┴└────┘
105 direct_limit.induction_on x $ λ i x, by rw lift_of; refl
id ┴ ┴ ┴
typ ┴ ┴ ┴
106
107 section totalize
108 open_locale classical
109 variables (G f)
110 noncomputable def totalize : Π i j, G i →ₗ[R] G j :=
id ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴
src └─┘ ┴
typ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴
111 λ i j, if h : i ≤ j then f i j h else 0
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
112 variables {G f}
113
114 lemma totalize_apply (i j x) :
115 totalize G f i j x = if h : i ≤ j then f i j h x else 0 :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
116 if h : i ≤ j
id └┘ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴ ┴
117 then by dsimp only [totalize]; rw [dif_pos h, dif_pos h]
id └──────┘ └─────┘ ┴ └─────┘ ┴
src └──────────┘└──────┘┴ └──┘└─────┘┴ └┘└─────┘┴ └─
typ └──────────┘└──────┘┴ └──┘└─────┘┴┴└┘└─────┘┴┴└─
doc └──────────┘ ┴ └──┘ ┴ └┘ ┴ └─
txt └──────────┘ ┴ └──┘ ┴ └┘ ┴ └─
par └──────────┘ ┴ └──┘ ┴ └┘ ┴ └─
pid └───┘└┘ ┴ └┘ ┴ └┘ ┴ ┴└
st └──────────────────────────┘└───────┘└─────────┘┴└
118 else by dsimp only [totalize]; rw [dif_neg h, dif_neg h, linear_map.zero_apply]
id └──────┘ └─────┘ ┴ └─────┘ ┴ └───────────────────┘
src ─┘ └──────────┘└──────┘┴ └──┘└─────┘┴ └┘└─────┘┴ └┘└───────────────────┘└┘
typ ─┘ └──────────┘└──────┘┴ └──┘└─────┘┴┴└┘└─────┘┴┴└┘└───────────────────┘└┘
doc ─┘ └──────────┘ ┴ └──┘ ┴ └┘ ┴ └┘ └┘
txt ─┘ └──────────┘ ┴ └──┘ ┴ └┘ ┴ └┘ └┘
par ─┘ └──────────┘ ┴ └──┘ ┴ └┘ ┴ └┘ └┘
pid ─┘ └───┘└┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴
st ─┘ └──────────────────────────┘└───────┘└─────────┘└─────────────────────┘┴┴
119 end totalize
120
121 lemma to_module_totalize_of_le {x : direct_sum ι G} {i j : ι}
id └────────┘ ┴ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴ ┴
122 (hij : i ≤ j) (hx : ∀ k ∈ x.support, k ≤ i) :
id ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴
src ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴
123 direct_sum.to_module R ι (G j) (λ k, totalize G f k j) x =
id └──────────────────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────────┘ └──────┘ ┴
typ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
124 f i j hij (direct_sum.to_module R ι (G i) (λ k, totalize G f k i) x) :=
id ┴ ┴ ┴ └─┘ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────────────────┘ └──────┘
typ ┴ ┴ ┴ └─┘ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
125 begin
st └─────
126 rw [← @dfinsupp.sum_single ι G _ _ _ x],
id └─────────────────┘ ┴ ┴ ┴
src └────┘ └─────────────────┘┴ ┴ └─────┘ ┴
typ └────┘ └─────────────────┘┴┴┴┴└─────┘┴┴
doc └────┘ ┴ ┴ └─────┘ ┴
txt └────┘ ┴ ┴ └─────┘ ┴
par └────┘ ┴ ┴ └─────┘ ┴
pid └──┘ ┴ ┴ └─────┘ ┴
st ───────────────────────────────────────┘└──
127 unfold dfinsupp.sum,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └───────────┘
st ────────────────────┘
128 simp only [linear_map.map_sum],
129 refine finset.sum_congr rfl (λ k hk, _),
st └─
130 rw direct_sum.single_eq_lof R k (x k),
id ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴┴┴ ┴ ┴┴┴┴
doc └─┘ ┴ ┴ ┴ ┴ ┴
txt └─┘ ┴ ┴ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ────┘ └────────┘
131 simp [totalize_apply, hx k hk, le_trans (hx k hk) hij, directed_system.map_map f]
id ┴ ┴
typ ┴ ┴
132 end
st └─┘
133
134 lemma of.zero_exact_aux {x : direct_sum ι G} (H : submodule.quotient.mk x = (0 : direct_limit G f)) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
135 ∃ j, (∀ k ∈ x.support, k ≤ j) ∧ direct_sum.to_module R ι (G j) (λ i, totalize G f i j) x = (0 : G j) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
136 nonempty.elim (by apply_instance) $ assume ind : ι,
id ┴
typ ┴
137 span_induction ((quotient.mk_eq_zero _).1 H)
138 (λ x ⟨i, j, hij, y, hxy⟩, let ⟨k, hik, hjk⟩ := directed_order.directed i j in
id ┴ ┴ ┴
typ ┴ ┴ ┴
139 ⟨k, begin
140 clear_,
141 subst hxy,
142 split,
143 { intros i0 hi0,
144 rw [dfinsupp.mem_support_iff, dfinsupp.sub_apply, ← direct_sum.single_eq_lof,
145 ← direct_sum.single_eq_lof, dfinsupp.single_apply, dfinsupp.single_apply] at hi0,
146 split_ifs at hi0 with hi hj hj, { rwa hi at hik }, { rwa hi at hik }, { rwa hj at hjk },
st └┘ └┘ └┘
147 exfalso, apply hi0, rw sub_zero },
st └┘
148 simp [linear_map.map_sub, totalize_apply, hik, hjk,
149 directed_system.map_map f, direct_sum.apply_eq_component,
150 direct_sum.component.of],
151 end⟩)
st └─┘
152 ⟨ind, λ _ h, (finset.not_mem_empty _ h).elim, linear_map.map_zero _⟩
id └─┘ ┴
typ └─┘ ┴
153 (λ x y ⟨i, hi, hxi⟩ ⟨j, hj, hyj⟩,
id ┴ ┴
typ ┴ ┴
154 let ⟨k, hik, hjk⟩ := directed_order.directed i j in
id ┴
typ ┴
155 ⟨k, λ l hl,
id ┴
typ ┴
156 (finset.mem_union.1 (dfinsupp.support_add hl)).elim
157 (λ hl, le_trans (hi _ hl) hik)
158 (λ hl, le_trans (hj _ hl) hjk),
159 by simp [linear_map.map_add, hxi, hyj,
160 to_module_totalize_of_le hik hi,
161 to_module_totalize_of_le hjk hj]⟩)
162 (λ a x ⟨i, hi, hxi⟩,
id ┴ ┴
typ ┴ ┴
163 ⟨i, λ k hk, hi k (dfinsupp.support_smul hk),
id ┴ ┴
typ ┴ ┴
164 by simp [linear_map.map_smul, hxi]⟩)
165
166 /-- A component that corresponds to zero in the direct limit is already zero in some
167 bigger module in the directed system. -/
168 theorem of.zero_exact {i x} (H : of R ι G f i x = 0) :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
169 ∃ j hij, f i j hij x = (0 : G j) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
170 let ⟨j, hj, hxj⟩ := of.zero_exact_aux H in
id ┴
typ ┴
171 if hx0 : x = 0 then ⟨i, le_refl _, by simp [hx0]⟩
id ┴ ┴
typ ┴ ┴
172 else
173 have hij : i ≤ j, from hj _ $
id ┴
typ ┴
174 by simp [direct_sum.apply_eq_component, hx0],
175 ⟨j, hij, by simpa [totalize_apply, hij] using hxj⟩
176
177 end direct_limit
178
179 end module
180
181
182 namespace add_comm_group
183
184 variables [Π i, add_comm_group (G i)]
id ┴ └┘ └┘ └┘ ┴
src └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴
185
186 /-- The direct limit of a directed system is the abelian groups glued together along the maps. -/
187 def direct_limit (f : Π i j, i ≤ j → G i → G j)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
188 [Π i j hij, is_add_group_hom (f i j hij)] [directed_system G f] : Type* :=
id ┴ ┴ └─┘ └──────────────┘ ┴ ┴ ┴ └─┘ └─────────────┘ ┴ ┴
src └──────────────┘ └─────────────┘
typ ┴ ┴ └─┘ └──────────────┘ ┴ ┴ ┴ └─┘ └─────────────┘ ┴ ┴
doc └──────────────┘ └─────────────┘
189 @module.direct_limit ℤ _ ι _ _ _ G _ _ _
id └─────────────────┘ ┴ ┴ ┴
src └─────────────────┘ ┴
typ └─────────────────┘ ┴ ┴ ┴
doc └─────────────────┘
190 (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij)
id ┴ ┴ └─┘ └────────────────────────────┘ ┴ ┴ ┴ └─┘
src └────────────────────────────┘
typ ┴ ┴ └─┘ └────────────────────────────┘ ┴ ┴ ┴ └─┘
191 ⟨directed_system.map_self f, directed_system.map_map f⟩
id └──────────────────────┘ ┴ └─────────────────────┘ ┴
src └──────────────────────┘ └─────────────────────┘
typ └──────────────────────┘ ┴ └─────────────────────┘ ┴
192
193 namespace direct_limit
194
195 variables (f : Π i j, i ≤ j → G i → G j)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
196 variables [Π i j hij, is_add_group_hom (f i j hij)] [directed_system G f]
id ┴ ┴ └─┘ └──────────────┘ ┴ ┴ └─┘ └─────────────┘
src └──────────────┘ └─────────────┘
typ ┴ ┴ └─┘ └──────────────┘ ┴ ┴ └─┘ └─────────────┘
doc └──────────────┘ └─────────────┘
197
198 lemma directed_system : module.directed_system G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij) :=
id └────────────────────┘ ┴ ┴ ┴ └─┘ └────────────────────────────┘ ┴ ┴ ┴ └─┘
src └────────────────────┘ └────────────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ └─┘ └────────────────────────────┘ ┴ ┴ ┴ └─┘
doc └────────────────────┘
199 ⟨directed_system.map_self f, directed_system.map_map f⟩
id └──────────────────────┘ ┴ └─────────────────────┘ ┴
src └──────────────────────┘ └─────────────────────┘
typ └──────────────────────┘ ┴ └─────────────────────┘ ┴
200
201 local attribute [instance] directed_system
id └─────────────┘
src └─────────────┘
typ └─────────────┘
202
203 instance : add_comm_group (direct_limit G f) :=
id └────────────┘ └──────────┘ ┴ ┴
src └────────────┘ └──────────┘
typ └────────────┘ └──────────┘ ┴ ┴
doc └──────────┘
204 module.direct_limit.add_comm_group G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij)
id └────────────────────────────────┘ ┴ ┴ ┴ └─┘ └────────────────────────────┘ ┴ ┴ ┴ └─┘
src └────────────────────────────────┘ └────────────────────────────┘
typ └────────────────────────────────┘ ┴ ┴ ┴ └─┘ └────────────────────────────┘ ┴ ┴ ┴ └─┘
205
206 set_option class.instance_max_depth 50
doc └──────────────────────┘
207
208 /-- The canonical map from a component to the direct limit. -/
209 def of (i) : G i → direct_limit G f :=
id ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘
typ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘
210 module.direct_limit.of ℤ ι G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij) i
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
211 variables {G f}
212
213 instance of.is_add_group_hom (i) : is_add_group_hom (of G f i) :=
id ┴ ┴
typ ┴ ┴
214 linear_map.is_add_group_hom _
215
216 @[simp] lemma of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
217 module.direct_limit.of_f
218
219 @[simp] lemma of_zero (i) : of G f i 0 = 0 := is_add_group_hom.map_zero _
id ┴ ┴
typ ┴ ┴
doc └──┘
220 @[simp] lemma of_add (i x y) : of G f i (x + y) = of G f i x + of G f i y := is_add_hom.map_add _ _ _
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
221 @[simp] lemma of_neg (i x) : of G f i (-x) = -of G f i x := is_add_group_hom.map_neg _ _
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
222 @[simp] lemma of_sub (i x y) : of G f i (x - y) = of G f i x - of G f i y := is_add_group_hom.map_sub _ _ _
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
223
224 @[elab_as_eliminator]
doc └────────────────┘
225 protected theorem induction_on {C : direct_limit G f → Prop} (z : direct_limit G f)
id ┴ ┴
typ ┴ ┴
226 (ih : ∀ i x, C (of G f i x)) : C z :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
227 module.direct_limit.induction_on z ih
228
229 /-- A component that corresponds to zero in the direct limit is already zero in some
230 bigger module in the directed system. -/
231 theorem of.zero_exact (i x) (h : of G f i x = 0) : ∃ j hij, f i j hij x = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
232 module.direct_limit.of.zero_exact h
233
234 variables (P : Type u₁) [add_comm_group P]
id └────────────┘
src └────────────┘
typ └────────────┘
235 variables (g : Π i, G i → P) [Π i, is_add_group_hom (g i)]
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
236 variables (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
237
238 variables (G f)
239 /-- The universal property of the direct limit: maps from the components to another abelian group
240 that respect the directed system structure (i.e. make some diagram commute) give rise
241 to a unique map out of the direct limit. -/
242 def lift : direct_limit G f → P :=
id ┴ ┴
typ ┴ ┴
243 module.direct_limit.lift ℤ ι G (λ i j hij, is_add_group_hom.to_linear_map $ f i j hij)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
244 (λ i, is_add_group_hom.to_linear_map $ g i) Hg
id ┴ ┴
typ ┴ ┴
245 variables {G f}
246
247 instance lift.is_add_group_hom : is_add_group_hom (lift G f P g Hg) :=
id ┴ ┴
typ ┴ ┴
248 linear_map.is_add_group_hom _
249
250 @[simp] lemma lift_of (i x) : lift G f P g Hg (of G f i x) = g i x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
251 module.direct_limit.lift_of _ _ _
252
253 @[simp] lemma lift_zero : lift G f P g Hg 0 = 0 := is_add_group_hom.map_zero _
id ┴ ┴
typ ┴ ┴
doc └──┘
254 @[simp] lemma lift_add (x y) : lift G f P g Hg (x + y) = lift G f P g Hg x + lift G f P g Hg y := is_add_hom.map_add _ _ _
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
255 @[simp] lemma lift_neg (x) : lift G f P g Hg (-x) = -lift G f P g Hg x := is_add_group_hom.map_neg _ _
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
256 @[simp] lemma lift_sub (x y) : lift G f P g Hg (x - y) = lift G f P g Hg x - lift G f P g Hg y := is_add_group_hom.map_sub _ _ _
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
257
258 lemma lift_unique (F : direct_limit G f → P) [is_add_group_hom F] (x) :
id ┴ ┴
typ ┴ ┴
259 F x = lift G f P (λ i x, F $ of G f i x) (λ i j hij x, by rw of_f) x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
260 direct_limit.induction_on x $ λ i x, by rw lift_of
id ┴ ┴
typ ┴ ┴
261
262 end direct_limit
263
264 end add_comm_group
265
266
267 namespace ring
268
269 variables [Π i, comm_ring (G i)]
id ┴ └┘ └┘ ┴
src └┘ └┘
typ ┴ └┘ └┘ ┴
270 variables (f : Π i j, i ≤ j → G i → G j)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
271 variables [Π i j hij, is_ring_hom (f i j hij)]
id ┴ ┴ └─┘ └─────────┘ ┴ ┴ └─┘
src └─────────┘
typ ┴ ┴ └─┘ └─────────┘ ┴ ┴ └─┘
doc └─────────┘
272 variables [directed_system G f]
id └─────────────┘
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
273
274 open free_comm_ring
275
276 /-- The direct limit of a directed system is the rings glued together along the maps. -/
277 def direct_limit : Type (max v w) :=
278 (ideal.span { a | (∃ i j H x, of (⟨j, f i j H x⟩ : Σ i, G i) - of ⟨i, x⟩ = a) ∨
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
279 (∃ i, of (⟨i, 1⟩ : Σ i, G i) - 1 = a) ∨
id ┴ ┴┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
280 (∃ i x y, of (⟨i, x + y⟩ : Σ i, G i) - (of ⟨i, x⟩ + of ⟨i, y⟩) = a) ∨
id ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
typ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
281 (∃ i x y, of (⟨i, x * y⟩ : Σ i, G i) - (of ⟨i, x⟩ * of ⟨i, y⟩) = a) }).quotient
id ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘
src ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──────┘
typ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘
282
283 namespace direct_limit
284
285 instance : comm_ring (direct_limit G f) :=
id └───────┘ └──────────┘ ┴ ┴
src └───────┘ └──────────┘
typ └───────┘ └──────────┘ ┴ ┴
doc └──────────┘
286 ideal.quotient.comm_ring _
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
287
288 instance : ring (direct_limit G f) :=
id └──┘ └──────────┘ ┴ ┴
src └──┘ └──────────┘
typ └──┘ └──────────┘ ┴ ┴
doc └──────────┘
289 comm_ring.to_ring _
id └───────────────┘
src └───────────────┘
typ └───────────────┘
290
291 /-- The canonical map from a component to the direct limit. -/
292 def of (i) (x : G i) : direct_limit G f :=
id ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘
typ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘
293 ideal.quotient.mk _ $ of ⟨i, x⟩
id └───────────────┘ └┘ ┴ ┴
src └───────────────┘ └┘
typ └───────────────┘ └┘ ┴ ┴
294
295 variables {G f}
296
297 instance of.is_ring_hom (i) : is_ring_hom (of G f i) :=
id └─────────┘ └┘ ┴ ┴ ┴
src └─────────┘ └┘
typ └─────────┘ └┘ ┴ ┴ ┴
doc └─────────┘ └┘
298 { map_one := ideal.quotient.eq.2 $ subset_span $ or.inr $ or.inl ⟨i, rfl⟩,
id └───────────────┘┴ └─────────┘ └────┘ └────┘ ┴ └─┘
src └───────────────┘┴ └─────────┘ └────┘ └────┘ └─┘
typ └───────────────┘┴ └─────────┘ └────┘ └────┘ ┴ └─┘
299 map_mul := λ x y, ideal.quotient.eq.2 $ subset_span $ or.inr $ or.inr $ or.inr ⟨i, x, y, rfl⟩,
id ┴ ┴ └───────────────┘┴ └─────────┘ └────┘ └────┘ └────┘ ┴ ┴ ┴ └─┘
src └───────────────┘┴ └─────────┘ └────┘ └────┘ └────┘ └─┘
typ ┴ ┴ └───────────────┘┴ └─────────┘ └────┘ └────┘ └────┘ ┴ ┴ ┴ └─┘
300 map_add := λ x y, ideal.quotient.eq.2 $ subset_span $ or.inr $ or.inr $ or.inl ⟨i, x, y, rfl⟩ }
id ┴ ┴ └───────────────┘┴ └─────────┘ └────┘ └────┘ └────┘ ┴ ┴ ┴ └─┘
src └───────────────┘┴ └─────────┘ └────┘ └────┘ └────┘ └─┘
typ ┴ ┴ └───────────────┘┴ └─────────┘ └────┘ └────┘ └────┘ ┴ ┴ ┴ └─┘
301
302 @[simp] lemma of_f {i j} (hij) (x) : of G f j (f i j hij x) = of G f i x :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └──┘ └┘ └┘
303 ideal.quotient.eq.2 $ subset_span $ or.inl ⟨i, j, hij, x, rfl⟩
id └───────────────┘┴ └─────────┘ └────┘ ┴ ┴ └─┘ ┴ └─┘
src └───────────────┘┴ └─────────┘ └────┘ └─┘
typ └───────────────┘┴ └─────────┘ └────┘ ┴ ┴ └─┘ ┴ └─┘
304
305 @[simp] lemma of_zero (i) : of G f i 0 = 0 := is_ring_hom.map_zero _
id └┘ ┴ ┴ ┴ ┴ └──────────────────┘
src └┘ ┴ └──────────────────┘
typ └┘ ┴ ┴ ┴ ┴ └──────────────────┘
doc └──┘ └┘ └──────────────────┘
306 @[simp] lemma of_one (i) : of G f i 1 = 1 := is_ring_hom.map_one _
id └┘ ┴ ┴ ┴ ┴ └─────────────────┘
src └┘ ┴ └─────────────────┘
typ └┘ ┴ ┴ ┴ ┴ └─────────────────┘
doc └──┘ └┘
307 @[simp] lemma of_add (i x y) : of G f i (x + y) = of G f i x + of G f i y := is_ring_hom.map_add _
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────────────────┘
src └┘ ┴ ┴ └┘ ┴ └┘ └─────────────────┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────────────────┘
doc └──┘ └┘ └┘ └┘
308 @[simp] lemma of_neg (i x) : of G f i (-x) = -of G f i x := is_ring_hom.map_neg _
id └┘ ┴ ┴ ┴ ┴┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ └─────────────────┘
src └┘ ┴ ┴ ┴└┘ └─────────────────┘
typ └┘ ┴ ┴ ┴ ┴┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ └─────────────────┘
doc └──┘ └┘ └┘ └─────────────────┘
309 @[simp] lemma of_sub (i x y) : of G f i (x - y) = of G f i x - of G f i y := is_ring_hom.map_sub _
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────────────────┘
src └┘ ┴ ┴ └┘ ┴ └┘ └─────────────────┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────────────────┘
doc └──┘ └┘ └┘ └┘ └─────────────────┘
310 @[simp] lemma of_mul (i x y) : of G f i (x * y) = of G f i x * of G f i y := is_ring_hom.map_mul _
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────────────────┘
src └┘ ┴ ┴ └┘ ┴ └┘ └─────────────────┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────────────────┘
doc └──┘ └┘ └┘ └┘
311 @[simp] lemma of_pow (i x) (n : ℕ) : of G f i (x ^ n) = of G f i x ^ n := is_semiring_hom.map_pow _ _ _
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘
src ┴ └┘ ┴ ┴ └┘ ┴ └─────────────────────┘
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘
doc └──┘ └┘ └┘
312
313 /-- Every element of the direct limit corresponds to some element in
314 some component of the directed system. -/
315 theorem exists_of (z : direct_limit G f) : ∃ i x, of G f i x = z :=
id └──────────┘ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ └┘ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────┘ └┘
316 nonempty.elim (by apply_instance) $ assume ind : ι,
id └───────────┘ ┴
src └───────────┘ └────────────┘
typ └───────────┘ └────────────┘ ┴
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
317 quotient.induction_on' z $ λ x, free_abelian_group.induction_on x
id └────────────────────┘ ┴ ┴ └─────────────────────────────┘ ┴
src └────────────────────┘ └─────────────────────────────┘
typ └────────────────────┘ ┴ ┴ └─────────────────────────────┘ ┴
318 ⟨ind, 0, of_zero ind⟩
id └─┘ └─────┘ └─┘
src └─────┘
typ └─┘ └─────┘ └─┘
319 (λ s, multiset.induction_on s
id ┴ └───────────────────┘ ┴
src └───────────────────┘
typ ┴ └───────────────────┘ ┴
320 ⟨ind, 1, of_one ind⟩
id └─┘ └────┘ └─┘
src └────┘
typ └─┘ └────┘ └─┘
321 (λ a s ih, let ⟨i, x⟩ := a, ⟨j, y, hs⟩ := ih, ⟨k, hik, hjk⟩ := directed_order.directed i j in
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
322 ⟨k, f i k hik x * f j k hjk y, by rw [of_mul, of_f, of_f, hs]; refl⟩))
id └──┘
src └──┘
typ └──┘
doc └──┘
323 (λ s ⟨i, x, ih⟩, ⟨i, -x, by rw [of_neg, ih]; refl⟩)
id ┴ ┴ └──┘
src └──┘
typ ┴ ┴ └──┘
doc └──┘
324 (λ p q ⟨i, x, ihx⟩ ⟨j, y, ihy⟩, let ⟨k, hik, hjk⟩ := directed_order.directed i j in
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
325 ⟨k, f i k hik x + f j k hjk y, by rw [of_add, of_f, of_f, ihx, ihy]; refl⟩)
id └──┘
src └──┘
typ └──┘
doc └──┘
326
327 @[elab_as_eliminator] theorem induction_on {C : direct_limit G f → Prop} (z : direct_limit G f)
id ┴ ┴
typ ┴ ┴
doc └────────────────┘
328 (ih : ∀ i x, C (of G f i x)) : C z :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
329 let ⟨i, x, hx⟩ := exists_of z in hx ▸ ih i x
id ┴ ┴
typ ┴ ┴
330
331 section of_zero_exact
332 open_locale classical
333 variables (G f)
334 lemma of.zero_exact_aux2 {x : free_comm_ring Σ i, G i} {s t} (hxs : is_supported x s) {j k}
id └────────────┘ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴
src └────────────┘ ┴ ┴ └──────────┘
typ └────────────┘ ┴ ┴┴ ┴ ┴ └──────────┘ ┴ ┴
335 (hj : ∀ z : Σ i, G i, z ∈ s → z.1 ≤ j) (hk : ∀ z : Σ i, G i, z ∈ t → z.1 ≤ k)
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
336 (hjk : j ≤ k) (hst : s ⊆ t) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
337 f j k hjk (lift (λ ix : s, f ix.1.1 j (hj ix ix.2) ix.1.2) (restriction s x)) =
id ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └┘┴ ┴ ┴ └┘ └┘ └┘┴ └┘┴ ┴ └─────────┘ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴
typ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └┘┴ ┴ ┴ └┘ └┘ └┘┴ └┘┴ ┴ └─────────┘ ┴ ┴ ┴
338 lift (λ ix : t, f ix.1.1 k (hk ix ix.2) ix.1.2) (restriction t x) :=
id └──┘ ┴ ┴ └┘┴ ┴ ┴ └┘ └┘ └┘┴ └┘┴ ┴ └─────────┘ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ └─────────┘
typ └──┘ ┴ ┴ └┘┴ ┴ ┴ └┘ └┘ └┘┴ └┘┴ ┴ └─────────┘ ┴ ┴
339 begin
340 refine ring.in_closure.rec_on hxs _ _ _ _,
341 { rw [restriction_one, lift_one, is_ring_hom.map_one (f j k hjk), restriction_one, lift_one] },
st ┴
342 { rw [restriction_neg, restriction_one, lift_neg, lift_one,
343 is_ring_hom.map_neg (f j k hjk), is_ring_hom.map_one (f j k hjk),
id ┴
typ ┴
344 restriction_neg, restriction_one, lift_neg, lift_one] },
st ┴ └┘
345 { rintros _ ⟨p, hps, rfl⟩ n ih,
346 rw [restriction_mul, lift_mul, is_ring_hom.map_mul (f j k hjk), ih, restriction_mul, lift_mul,
id ┴ ┴
typ ┴ ┴
347 restriction_of, dif_pos hps, lift_of, restriction_of, dif_pos (hst hps), lift_of],
348 dsimp only, rw directed_system.map_map f, refl },
st └┘
349 { rintros x y ihx ihy,
350 rw [restriction_add, lift_add, is_ring_hom.map_add (f j k hjk), ihx, ihy, restriction_add, lift_add] }
id ┴ ┴
typ ┴ ┴
st ┴ └─
351 end
st ──┘
352 variables {G f}
353
354 lemma of.zero_exact_aux {x : free_comm_ring Σ i, G i} (H : ideal.quotient.mk _ x = (0 : direct_limit G f)) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
355 ∃ j s, ∃ H : (∀ k : Σ i, G i, k ∈ s → k.1 ≤ j), is_supported x s ∧
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
356 lift (λ ix : s, f ix.1.1 j (H ix ix.2) ix.1.2) (restriction s x) = (0 : G j) :=
id ┴ ┴
typ ┴ ┴
357 begin
358 refine span_induction (ideal.quotient.eq_zero_iff_mem.1 H) _ _ _ _,
359 { rintros x (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩),
360 { refine ⟨j, {⟨i, x⟩, ⟨j, f i j hij x⟩}, _,
id ┴ ┴ ┴
typ ┴ ┴ ┴
361 is_supported_sub (is_supported_of.2 $ or.inl rfl) (is_supported_of.2 $ or.inr $ or.inl rfl), _⟩,
362 { rintros k (rfl | ⟨rfl | h⟩), refl, exact hij, cases h },
st └┘
363 { rw [restriction_sub, lift_sub, restriction_of, dif_pos, restriction_of, dif_pos, lift_of, lift_of],
364 dsimp only, rw directed_system.map_map f, exact sub_self _,
365 { left, refl }, { right, left, refl }, } },
st └┘ └┘ └──┘
366 { refine ⟨i, {⟨i, 1⟩}, _, is_supported_sub (is_supported_of.2 $ or.inl rfl) is_supported_one, _⟩,
id ┴
typ ┴
367 { rintros k (rfl | h), refl, cases h },
st └┘
368 { rw [restriction_sub, lift_sub, restriction_of, dif_pos, restriction_one, lift_of, lift_one],
369 dsimp only, rw [is_ring_hom.map_one (f i i _), sub_self], exact _inst_7 i i _, { left, refl } } },
id ┴ ┴
typ ┴ ┴
st └────┘
370 { refine ⟨i, {⟨i, x+y⟩, ⟨i, x⟩, ⟨i, y⟩}, _,
id ┴ ┴ ┴
typ ┴ ┴ ┴
371 is_supported_sub (is_supported_of.2 $ or.inr $ or.inr $ or.inl rfl)
372 (is_supported_add (is_supported_of.2 $ or.inr $ or.inl rfl) (is_supported_of.2 $ or.inl rfl)), _⟩,
373 { rintros k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩), refl, refl, refl, cases hk },
st └┘
374 { rw [restriction_sub, restriction_add, restriction_of, restriction_of, restriction_of,
375 dif_pos, dif_pos, dif_pos, lift_sub, lift_add, lift_of, lift_of, lift_of],
376 dsimp only, rw is_ring_hom.map_add (f i i _), exact sub_self _,
id ┴
typ ┴
377 { right, right, left, refl }, { apply_instance }, { left, refl }, { right, left, refl } } },
st └┘ └┘ └┘ └────┘
378 { refine ⟨i, {⟨i, x*y⟩, ⟨i, x⟩, ⟨i, y⟩}, _,
id ┴ ┴ ┴
typ ┴ ┴ ┴
379 is_supported_sub (is_supported_of.2 $ or.inr $ or.inr $ or.inl rfl)
380 (is_supported_mul (is_supported_of.2 $ or.inr $ or.inl rfl) (is_supported_of.2 $ or.inl rfl)), _⟩,
381 { rintros k (rfl | ⟨rfl | ⟨rfl | hk⟩⟩), refl, refl, refl, cases hk },
st └┘
382 { rw [restriction_sub, restriction_mul, restriction_of, restriction_of, restriction_of,
383 dif_pos, dif_pos, dif_pos, lift_sub, lift_mul, lift_of, lift_of, lift_of],
384 dsimp only, rw is_ring_hom.map_mul (f i i _), exact sub_self _,
id ┴
typ ┴
385 { right, right, left, refl }, { apply_instance }, { left, refl }, { right, left, refl } } } },
st └┘ └┘ └┘ └──────┘
386 { refine nonempty.elim (by apply_instance) (assume ind : ι, _),
id ┴
typ ┴
387 refine ⟨ind, ∅, λ _, false.elim, is_supported_zero, _⟩,
id └─┘
typ └─┘
388 rw [restriction_zero, lift_zero] },
st ┴ └┘
389 { rintros x y ⟨i, s, hi, hxs, ihs⟩ ⟨j, t, hj, hyt, iht⟩,
390 rcases directed_order.directed i j with ⟨k, hik, hjk⟩,
id ┴ ┴
typ ┴ ┴
391 have : ∀ z : Σ i, G i, z ∈ s ∪ t → z.1 ≤ k,
id ┴ ┴ ┴
typ ┴ ┴ ┴
392 { rintros z (hz | hz), exact le_trans (hi z hz) hik, exact le_trans (hj z hz) hjk },
st └┘
393 refine ⟨k, s ∪ t, this, is_supported_add (is_supported_upwards hxs $ set.subset_union_left s t)
id ┴
typ ┴
394 (is_supported_upwards hyt $ set.subset_union_right s t), _⟩,
395 { rw [restriction_add, lift_add,
396 ← of.zero_exact_aux2 G f hxs hi this hik (set.subset_union_left s t),
id ┴
typ ┴
397 ← of.zero_exact_aux2 G f hyt hj this hjk (set.subset_union_right s t),
id ┴
typ ┴
398 ihs, is_ring_hom.map_zero (f i k hik), iht, is_ring_hom.map_zero (f j k hjk), zero_add] } },
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st ┴ └──┘
399 { rintros x y ⟨j, t, hj, hyt, iht⟩, rw smul_eq_mul,
400 rcases exists_finset_support x with ⟨s, hxs⟩,
401 rcases (s.image sigma.fst).exists_le with ⟨i, hi⟩,
402 rcases directed_order.directed i j with ⟨k, hik, hjk⟩,
id ┴ ┴
typ ┴ ┴
403 have : ∀ z : Σ i, G i, z ∈ ↑s ∪ t → z.1 ≤ k,
id ┴ ┴ ┴
typ ┴ ┴ ┴
404 { rintros z (hz | hz), exact le_trans (hi z.1 $ finset.mem_image.2 ⟨z, hz, rfl⟩) hik, exact le_trans (hj z hz) hjk },
st └┘
405 refine ⟨k, ↑s ∪ t, this, is_supported_mul (is_supported_upwards hxs $ set.subset_union_left ↑s t)
id ┴
typ ┴
406 (is_supported_upwards hyt $ set.subset_union_right ↑s t), _⟩,
407 rw [restriction_mul, lift_mul,
408 ← of.zero_exact_aux2 G f hyt hj this hjk (set.subset_union_right ↑s t),
id ┴
typ ┴
409 iht, is_ring_hom.map_zero (f j k hjk), mul_zero] }
id ┴ ┴
typ ┴ ┴
st ┴ └─
410 end
st ──┘
411
412 /-- A component that corresponds to zero in the direct limit is already zero in some
413 bigger module in the directed system. -/
414 lemma of.zero_exact {i x} (hix : of G f i x = 0) : ∃ j, ∃ hij : i ≤ j, f i j hij x = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
415 let ⟨j, s, H, hxs, hx⟩ := of.zero_exact_aux hix in
id ┴
typ ┴
416 have hixs : (⟨i, x⟩ : Σ i, G i) ∈ s, from is_supported_of.1 hxs,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
417 ⟨j, H ⟨i, x⟩ hixs, by rw [restriction_of, dif_pos hixs, lift_of] at hx; exact hx⟩
id ┴ ┴
typ ┴ ┴
418 end of_zero_exact
419
420 /-- If the maps in the directed system are injective, then the canonical maps
421 from the components to the direct limits are injective. -/
422 theorem of_inj (hf : ∀ i j hij, function.injective (f i j hij)) (i) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
423 function.injective (of G f i) :=
id ┴ ┴
typ ┴ ┴
424 begin
425 suffices : ∀ x, of G f i x = 0 → x = 0,
id ┴ ┴ ┴
typ ┴ ┴ ┴
426 { intros x y hxy, rw ← sub_eq_zero_iff_eq, apply this,
427 rw [is_ring_hom.map_sub (of G f i), hxy, sub_self] },
id ┴ ┴
typ ┴ ┴
st ┴ └┘
428 intros x hx, rcases of.zero_exact hx with ⟨j, hij, hfx⟩,
429 apply hf i j hij, rw [hfx, is_ring_hom.map_zero (f i j hij)]
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st ┴
430 end
st └─┘
431
432 variables (P : Type u₁) [comm_ring P]
id └───────┘
src └───────┘
typ └───────┘
433 variables (g : Π i, G i → P) [Π i, is_ring_hom (g i)]
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
434 variables (Hg : ∀ i j hij x, g j (f i j hij x) = g i x)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
435 include Hg
436
437 open free_comm_ring
438
439 variables (G f)
440 /-- The universal property of the direct limit: maps from the components to another ring
441 that respect the directed system structure (i.e. make some diagram commute) give rise
442 to a unique map out of the direct limit. -/
443 def lift : direct_limit G f → P :=
id ┴ ┴
typ ┴ ┴
444 ideal.quotient.lift _ (free_comm_ring.lift $ λ x, g x.1 x.2) begin
445 suffices : ideal.span _ ≤
446 ideal.comap (free_comm_ring.lift (λ (x : Σ (i : ι), G i), g (x.fst) (x.snd))) ⊥,
id ┴ ┴
typ ┴ ┴
447 { intros x hx, exact (mem_bot P).1 (this hx) },
id ┴
typ ┴
st └┘
448 rw ideal.span_le, intros x hx,
449 rw [mem_coe, ideal.mem_comap, mem_bot],
450 rcases hx with ⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩;
451 simp only [lift_sub, lift_of, Hg, lift_one, lift_add, lift_mul,
452 is_ring_hom.map_one (g i), is_ring_hom.map_add (g i), is_ring_hom.map_mul (g i), sub_self]
id ┴ ┴ ┴
typ ┴ ┴ ┴
453 end
st └─┘
454 variables {G f}
455 omit Hg
456
457 instance lift.is_ring_hom : is_ring_hom (lift G f P g Hg) :=
id ┴ ┴
typ ┴ ┴
458 ⟨free_comm_ring.lift_one _,
459 λ x y, quotient.induction_on₂' x y $ λ p q, free_comm_ring.lift_mul _ _ _,
460 λ x y, quotient.induction_on₂' x y $ λ p q, free_comm_ring.lift_add _ _ _⟩
461
462 @[simp] lemma lift_of (i x) : lift G f P g Hg (of G f i x) = g i x := free_comm_ring.lift_of _ _
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
463 @[simp] lemma lift_zero : lift G f P g Hg 0 = 0 := is_ring_hom.map_zero _
id ┴ ┴
typ ┴ ┴
doc └──┘
464 @[simp] lemma lift_one : lift G f P g Hg 1 = 1 := is_ring_hom.map_one _
id ┴ ┴
typ ┴ ┴
doc └──┘
465 @[simp] lemma lift_add (x y) : lift G f P g Hg (x + y) = lift G f P g Hg x + lift G f P g Hg y := is_ring_hom.map_add _
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
466 @[simp] lemma lift_neg (x) : lift G f P g Hg (-x) = -lift G f P g Hg x := is_ring_hom.map_neg _
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
467 @[simp] lemma lift_sub (x y) : lift G f P g Hg (x - y) = lift G f P g Hg x - lift G f P g Hg y := is_ring_hom.map_sub _
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
468 @[simp] lemma lift_mul (x y) : lift G f P g Hg (x * y) = lift G f P g Hg x * lift G f P g Hg y := is_ring_hom.map_mul _
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
469 @[simp] lemma lift_pow (x) (n : ℕ) : lift G f P g Hg (x ^ n) = lift G f P g Hg x ^ n := is_semiring_hom.map_pow _ _ _
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
470
471 theorem lift_unique (F : direct_limit G f → P) [is_ring_hom F] (x) :
id ┴ ┴
typ ┴ ┴
472 F x = lift G f P (λ i x, F $ of G f i x) (λ i j hij x, by rw [of_f]) x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ┴
473 direct_limit.induction_on x $ λ i x, by rw lift_of
id ┴ ┴
typ ┴ ┴
474
475 end direct_limit
476
477 end ring
478
479
480 namespace field
481
482 variables [Π i, field (G i)]
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
483 variables (f : Π i j, i ≤ j → G i → G j) [Π i j hij, is_ring_hom (f i j hij)]
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴ ┴ └─┘
src ┴ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴ ┴ └─┘
doc └─────────┘
484 variables [directed_system G f]
id └─────────────┘
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
485
486 namespace direct_limit
487
488 instance nonzero_comm_ring : nonzero_comm_ring (ring.direct_limit G f) :=
id └───────────────┘ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ └───────────────┘ └───────────────┘ ┴ ┴
doc └───────────────┘ └───────────────┘
489 { zero_ne_one := nonempty.elim (by apply_instance) $ assume i : ι, begin
id └───────────┘ ┴
src └───────────┘ └────────────┘
typ └───────────┘ └────────────┘ ┴
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
490 change (0 : ring.direct_limit G f) ≠ 1,
491 rw ← ring.direct_limit.of_one,
492 intros H, rcases ring.direct_limit.of.zero_exact H.symm with ⟨j, hij, hf⟩,
id ┴ ┴
src ┴ ┴
typ ┴ ┴
493 rw is_ring_hom.map_one (f i j hij) at hf,
id ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ └─┘
494 exact one_ne_zero hf
id └─────────┘ └┘
src └─────────┘
typ └─────────┘ └┘
495 end,
st └─┘
496 .. ring.direct_limit.comm_ring G f }
id └─────────────────────────┘ ┴ ┴
src └─────────────────────────┘
typ └─────────────────────────┘ ┴ ┴
497
498 theorem exists_inv {p : ring.direct_limit G f} : p ≠ 0 → ∃ y, p * y = 1 :=
id └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └───────────────┘ ┴ ┴ ┴ ┴ ┴
typ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └───────────────┘
499 ring.direct_limit.induction_on p $ λ i x H,
id └────────────────────────────┘ ┴ ┴ ┴ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴ ┴ ┴ ┴
500 ⟨ring.direct_limit.of G f i (x⁻¹), by erw [← ring.direct_limit.of_mul,
id └──────────────────┘ ┴ ┴ ┴ ┴└┘
src └──────────────────┘ └┘
typ └──────────────────┘ ┴ ┴ ┴ ┴└┘
doc └──────────────────┘
501 mul_inv_cancel (assume h : x = 0, H $ by rw [h, ring.direct_limit.of_zero]),
st ┴
502 ring.direct_limit.of_one]⟩
st ┴
503
504 section
505 open_locale classical
506
507 noncomputable def inv (p : ring.direct_limit G f) : ring.direct_limit G f :=
id └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
doc └───────────────┘ └───────────────┘
508 if H : p = 0 then 0 else classical.some (direct_limit.exists_inv G f H)
id └┘ ┴ ┴ └────────────┘ ┴ ┴ ┴
src └┘ ┴ └────────────┘
typ └┘ ┴ ┴ └────────────┘ ┴ ┴ ┴
509
510 protected theorem mul_inv_cancel {p : ring.direct_limit G f} (hp : p ≠ 0) : p * inv G f p = 1 :=
id └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └───────────────┘ ┴ ┴ └─┘ ┴
typ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
doc └───────────────┘
511 by rw [inv, dif_neg hp, classical.some_spec (direct_limit.exists_inv G f hp)]
512
513 protected theorem inv_mul_cancel {p : ring.direct_limit G f} (hp : p ≠ 0) : inv G f p * p = 1 :=
id └───────────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ ┴ └─┘ ┴ ┴
typ └───────────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘
514 by rw [_root_.mul_comm, direct_limit.mul_inv_cancel G f hp]
515
516 protected noncomputable def field : field (ring.direct_limit G f) :=
id └───┘ └───────────────┘ ┴ ┴
src └───┘ └───────────────┘
typ └───┘ └───────────────┘ ┴ ┴
doc └───────────────┘
517 { inv := inv G f,
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
518 mul_inv_cancel := λ p, direct_limit.mul_inv_cancel G f,
id ┴ ┴ ┴
typ ┴ ┴ ┴
519 inv_mul_cancel := λ p, direct_limit.inv_mul_cancel G f,
id ┴ ┴ ┴
typ ┴ ┴ ┴
520 .. direct_limit.nonzero_comm_ring G f }
id └────────────────────────────┘ ┴ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴ ┴
521
522 protected noncomputable def discrete_field : discrete_field (ring.direct_limit G f) :=
id └────────────┘ └───────────────┘ ┴ ┴
src └────────────┘ └───────────────┘
typ └────────────┘ └───────────────┘ ┴ ┴
doc └───────────────┘
523 { has_decidable_eq := classical.dec_eq _,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
524 inv_zero := dif_pos rfl,
id └─────┘ └─┘
src └─────┘ └─┘
typ └─────┘ └─┘
525 ..direct_limit.field G f }
id └────────────────┘ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴
526
527 end
528
529 end direct_limit
530
531 end field